-----------------------------------------------------------------------------
--
-- Module      :  Dist
-- Copyright   :
-- License     :  AllRightsReserved
--
-- Maintainer  :
-- Stability   :
-- Portability :
--
-- |
--
-----------------------------------------------------------------------------

module Dist where

import POrd
import Cpo

-- Eine Distanz kann entweder Infinity sein oder 
-- einen Integer-Wert mit der Anzahl der Schritte enthalten
data Dist = Value Int | Infinity
    deriving(Eq,Show)

add :: Dist -> Int -> Dist
add d i = case d of
                Infinity -> Infinity
                Value distVal -> Value (distVal + 1)

-- Infinity ist das groesste Element, ansonsten ist eine 
-- Distanz kleiner, je weniger Schritte benoetigt werden
instance POrd Dist where
    _ `ple` Infinity = True
    Infinity `ple` _ = False
    (Value m1) `ple` (Value m2) = m1 <= m2

-- das kleinste Element in unserer CPO ist die 0, das groesste Infinity
-- hier gibt es einen Konflikt mit der Spezifikation, der sich aus folgender Problemstellung ergibt:
-- 1) der initiale Zustand soll kleiner sein als die Loesung
--    der initiale Zustand enthaelt lauter Infinity-Entfernungen
--    daraus folgt, dass Infinity kleiner sein muss als Entfernungen mit Int-Wert
-- 2) bei der Berechnung der Entfernungen wird der minimale Wert (min) genommen
--    hier darf Infinity nicht kleiner sein als andere Werte, sondern muss der groesste Wert sein
--    daraus ergibt sich, dass Infinity einmal das kleinste und einmal das Groesste Element sein soll.
instance Cpo Dist where
    bottom      = Value 0
    Infinity `lub` m2 = Infinity
    m1 `lub` Infinity = Infinity
    (Value m1) `lub` (Value m2) =
        if m1 >= m2 then
            Value m1
        else
            Value m2



